This section describes our implementation of OIGJ:
the language syntax (\Ref{Section}{Annotations}) and the type-checker implementation (\Ref{Section}{Implementation}).
\Ref{Section}{CaseStudy} presents our case study
    that involved annotating Sun's implementation
    of the \code{java.util} collections, and our conclusions about the
    design of the collection classes
    w.r.t.\
    %with respect to
    ownership and immutability.

The prototype OIGJ type-checker is implemented and distributed as part of the Checker Framework~\cite{PapiACPE2008}\footnote{\url{http://types.cs.washington.edu/checker-framework/}},
    which supports pluggable type systems using type annotations.


\Subsection[Annotations]{Syntax: from generics to annotations}

Whereas this paper uses generics to express ownership and immutability
(e.g., \code{Date<O,I>}), our OIGJ implementation uses Java 7's type
annotations~\cite{JSR308-2008-09-12} (e.g., \code{@O @I Date}).  Java 7's receiver annotations
play the role of cJ's guards.

% {I think we should use JSR 308 receiver annotations throughout, and
%  not have to describe them here (currently commented out).  -MDE}
% Yoav: that's a big change, I'll see if I have the time...

% Finally, OIGJ's generics syntax is built on top of cJ, e.g.,
% \begin{algorithmic}
% \STATE \code{\underline{@ReadOnly} Date<I> getDate() \lb \ldots \rb}
% \end{algorithmic}
% On the other hand, OIGJ's type annotations syntax uses instead an annotation on \this,
%     with the following syntax:
% \begin{algorithmic}
% \STATE \code{@I Date getDate() \underline{@ReadOnly} \lb \ldots \rb}
% \end{algorithmic}

% The annotation choice is the same as that for IGJ~\cite{PapiACPE2008}.

% \paragraph{Review of annotations in IGJ~\cite{PapiACPE2008}}
% IGJ was originally implemented using generics syntax~\cite{ZibinPAAKE2007}
%     and later using \emph{type annotations} syntax~\cite{PapiACPE2008}.
% For example, instead of using generics, e.g., \code{Date<ReadOnly>},
%     to specify the immutability,
%     the programmer uses type annotations, e.g.,
%     \code{@ReadOnly Date}.
% Note that while Java~5 supports method and field annotations,
%     it does not support annotations on \emph{types}, e.g., on generic parameters
%     and arguments, receivers, external clauses, etc.
% JSR~308~\cite{JSR308-2008-09-12}, planned for Java~7, supports \emph{type annotations},
%     and the ability to plugin type annotation processors into \code{javac}.

Using annotations has the advantage of compatibility with existing
compilers and other tools.
Another advantage is the ability to use a default value, such as \code{@Mutable}.
Furthermore, it is possible to customize these defaults per class.
Defaults are not possible in generics, because a programmer must supply arguments for all
    generic parameters.

Using annotations has the disadvantage that
    some notions are no longer explicit in the syntax,
    such as transitivity, wildcards, and generic methods.
For example, compare the annotation and generic syntax:
\begin{algorithmic}
\STATE \code{class Foo~~~~~~\lb~@O @I Bar bar;~\rb}
\STATE \code{class Foo<O,I>~\lb~Bar<O,I>~ bar;~\rb}
\end{algorithmic}
Note that the type of \code{new Foo<World,Immut>().bar}
    is explicit in the generic syntax, whereas
    the annotation syntax (\code{new @World @Immut Foo().bar}) requires additional rules that mimic generics.
Use of annotations also complicates the implementation (see below).
For practical use, the compatibility benefits of using annotations outweigh
    their disadvantages.

\textbf{OIGJ's annotations} are the Cartesian product of
    owner parameters
    and immutability parameters.
Our implementation does not yet support wildcards (though in practice the
\code{@I} and \code{@O} annotations subsume most need for wildcards),
    nor classes with multiple
    owner or immutability parameters,
    such as \code{Iterator<O,\underline{ItrI,CollectionI},E>} in \Ref{Figure}{OIGJ-LinkedList}. % or \Ref{Figure}{OIGJ-Visitor-pattern}.
(In our case study, we implemented iterators using a single immutability parameter by declaring \code{next()} as mutable.)

A class declaration can be annotated as \code{@Immut} to indicate class
    immutability, i.e., all instances are immutable and no mutable methods exist.

% how do we handle multiple cJ guards, e.g., for iterators?
% void remove() @Mutable("ListItr")

%{Should we gloss over this?  We could mention it briefly and then and
%  just use separate annotations in the paper.  But, we don't want too many
%  caveats about ``what we show is not what we did'', and it seems pretty
%  minor, so we can leave it as is.}

%static <E> void copy(@OReadOnly("CO") Collection<E> src, @OMutable("CO") Collection<E> target)
%And if you use  @OI  then you can have two string arguments: @OI("O2","I2")

% For generic methods: have a string parameter
% Similarly to IGJ's type annotation syntax, generic methods uses a string parameter.


\Subsection[Implementation]{OIGJ implementation}

Because a pluggable type checker augments, rather than replaces, the type
system of the underlying language, the Checker Framework
permits only language extensions that are stricter than ordinary Java.
    A pluggable type system cannot relax Java's rules, as the OIGJ
    subtyping rule does.
For example,

\begin{algorithmic}
\STATE \code{\underline{@Immut} ~~~List<\underline{@Immut} ~~~\underline{Date}> ~~a;}
\STATE \code{\underline{@ReadOnly}~List<\underline{@ReadOnly}~Date> ~~b=a;} \myCOMMENT{OK}
\STATE \code{@Immut ~~~List<@Immut ~~~\underline{Object}> c=a;} \myCOMMENT{Illegal!}
\end{algorithmic}
The assignment \code{c=a} is illegal in Java and therefore in the
    Checker Framework, though it is legal in OIGJ itself.
Phrased differently, in our implementation, the covariance is limited to annotations.

% Next, we discuss the implementation details of the OIGJ compiler.  The
% prototype implementation~\cite{potanin:www:oigj} has 1600 lines of
% code, and the implementation of the ownership nesting rule and generic
% methods with immutability and owner parameters is still work in
% progress.
%
% The main complication of basing the implementation on the JSR~308
%     Checker Framework~\cite{JSR308-2008-09-12} as opposed to extending the
%     \texttt{javac} compiler directly~\cite{PotaninNCB2006,ZibinPAAKE2007},
%     was the need to emulate generic parameters
%     using annotations.
% We could not rely on the compiler handling all the
%     generic type variable cases for ownership and immutability.
% For example, in our implementation one uses the \verb+@OI+ annotation instead
%     of \verb+<O,I>+ generic type parameters that could be automatically handled by the
%     generics mechanism of the compiler.
% However, this limitation is outweighed by the compatibility benefits of using annotations.

% 600 lines of code is computed by subtracting the following two numbers:
% sloccount  checkers/src/checkers/oigj/ | grep oigj
% sloccount  checkers/oigj/quals/ | grep quals

The OIGJ type-checker incorporates, extends, and in some places overrides
the IGJ checker, and adds OGJ features.  It consists of about 700 source lines of
code (of which 100 lines is Java boilerplate to define the annotations).
Most of the code handles
default and implicit types.
%todo{Is this still accurate?  Can Mahmood improve it?}
% I don't know, ask Mahmood...

%For example, every string literal is
%immutable, and every local variable is initially set to be readonly (then
%refined by a built-in flow-sensitive analysis).

% Compared to the IGJ implementation in the Checker Framework,
% an implementation that directly modifies the
% \texttt{javac} compiler~\cite{PotaninNCB2006,ZibinPAAKE2007} can
% reuse the generics type mechanisms for free, but at the cost of
% incompatibility with existing Java programs, with IDEs and other compilers,
% and with newer versions of the modified compiler.


\Subsection[CaseStudy]{\normalcode{java.util} collections case study}

As a case study, we type-checked Sun's implementations of the
\code{java.util} collections (77 classes, 33,246 lines of code).
% out of 97 classes, leaving aside utility classes, such as
% \texttt{JapaneseImperialCalendar}, etc.
%    changed the \verb+clone+ method in 15 classes
%    (as described in \Ref{Section}{clone}),
This required us to write 85 \emph{ownership-related} annotations
and 46 \emph{immutability-related} annotations in 102 lines of code
    (the lines with \texttt{new} usually contain 2 annotations).

%
% The breakdown is roughly as follows:
%   46 Immutability annotations
%     33  I
%     9   ReadOnly
%     5   Mutable
%
%   85 Ownership annotations
%     54  O
%     31  Modifier
%

%    We also replaced all \emph{for-each-loops} with normal \emph{for-loops}.\footnote{
%   The new \emph{for-each} loop, introduced in Java~5,
%    has a circular dependency between \smallcode{java.util} and \smallcode{java.lang}:
%    interface \smallcode{Iterator} is defined in \smallcode{java.util},
%    however interface \smallcode{Iterable} refers to it and is defined in \smallcode{java.lang}.
%Therefore, in order to compile our version of \smallcode{Iterator} with ownership
% and immutability support,
%    we had to replace all new for-each loops with normal for-loops.
%{Couldn't we just annotate \code{Iterable}?  Then we could leave
%  off the entire footnote and the sentence it is attached to.}
%Yoav: It is a minor point, so I removed the entire 'for-each loop' thing.

Sun's collections are not type-safe with respect to generics
    because Java does not support generic arrays.
However, the OIGJ implementation uses type annotations, which
    can be placed on arrays as well,
    and therefore our annotated collections type-check without any errors
    with respect to ownership and immutability.

Class \code{LinkedList} in \Ref{Figure}{OIGJ-LinkedList}
    is similar in essence to Sun's implementation.
We annotated the constructors with \Raw{},
    thus allowing creation of immutable instances.
Since all instances of \code{Entry} are \this-owned,
    using \code{@This @I} as the default annotation for \code{Entry}
    meant that only three \emph{ownership-related}\footnote{%
        The other annotations are immutability-related, e.g., receiver annotations.}
    annotations were needed in \code{LinkedList}:

% \vbox prevents a column/page break
\vbox{\begin{algorithmic}
\STATE \code{\underline{@Default(\lb This.class}, I.class\rb)}
\STATE \code{static class Entry<E> \lb}
\STATE \code{~~E element; \underline{@O} Entry<E> next; \underline{@O} Entry<E> prev;}
\STATE \code{~~\ldots~\rb}
\end{algorithmic}}

Similarly, in a \code{HashMap}, both the array and the entries are \this-owned:
    \code{~~@This @I Entry[@This @I] table;}

The case study supports these conclusions:
    (i)~the collections classes are properly encapsulated (they own their representation),
    (ii)~it is possible to create immutable instances
        (all constructors are \Raw{}),
    and~(iii)~methods \code{Map.get} and \code{clone} contain design
    mistakes (see below).
%Interestingly, the two mistakes involve immutability (in method \code{get})
%    and ownership (in method \code{clone}).
We were not previously aware of these design mistakes.
We believe that if the collections were designed with ownership and immutability
    in mind, such mistakes could be avoided.


\newcommand{\ConcurrentModificationException}{\code{Concurrent\discretionary{-}{}{}Modification\discretionary{-}{}{}Exception}}

\paragraph{Immutability of method \normalcode{get}}
Let's start with a quick riddle:
    is there a \code{Map} implementation in \code{java.util}
    that might throw an exception when running the following \emph{single-threaded}
    code?

\begin{algorithmic}
\STATE \code{for (Object key : map.keySet()) \lb~map.get(key); \rb}
\end{algorithmic}
The answer is that for a map created with

\begin{algorithmic}
\STATE \code{new LinkedHashMap(100, 1, /*accessOrder=*/ true)}
\end{algorithmic}
    that contains more than one element,
    the above code throws \ConcurrentModificationException{}
    after printing one element.

Most programmers assume that \code{Map.get} is readonly,
    but there is no such guarantee in Java's specification.
%In fact, the above constructor of \code{LinkedHashMap} passes \code{true}
%    for the parameter \code{accessOrder} that specify the ordering mode:
%     \code{true} for access-order, \code{false} for insertion-order.
The documentation of \code{LinkedHashMap} states:
``\emph{A special constructor is provided to create a linked hash map whose order of iteration
    is the order in which its entries were last accessed,
    from least-recently accessed to most-recently (\emph{access-order}).
%This kind of map is well-suited to building LRU caches.
Invoking the \code{put} or {\code{get}} method results in an access to the corresponding entry.}''

Because calling \code{get} modified the list,
    the above code threw \ConcurrentModificationException.
Phrased differently, method \code{LinkedHashMap.get} is mutable!
Because an overriding method can only strengthen the specification of the
    overridden method, \code{HashMap.get} and \code{Map.get} must be mutable as well.

% \textbf{Method overriding rule} requires that the immutability of all \code{get}
% implementations must be mutable as well.


\paragraph{Ownership and method \normalcode{clone}}
Method \code{clone} violates owner-as-dominator because it leaks \this-owned references
    by creating a shallow copy,
    i.e., only immediate fields are copied.
Furthermore, Sun's implementation of \code{LinkedList} assigns to \code{\underline{result}.header},
    which is a \this-owned field.
This violates \textbf{Field assignment rule} of \Ref{Section}{typing-rules}, which only permits assignment to
    \code{\underline{this}.header}.

\begin{algorithmic}
\STATE ~\myCOMMENT{The following code appears in \code{LinkedList.clone()}.}
\STATE ~\myCOMMENT{Calling \code{super.clone()} breaks owner-as-dominator because}
\STATE ~\myCOMMENT{it leaked \code{this.header} to \code{result.header}.}
\STATE \code{LinkedList result = (LinkedList) super.clone();} \label{clone:cast}
\STATE \code{\underline{result}.header = new Entry();} \myCOMMENT{Illegal in OIGJ!} \label{clone:illegal}
\end{algorithmic}

We sketch a solution that, instead of initializing the cloned \code{result}
    from \this, uses the idea of \emph{inversion of control}.
The solution has two parts.
(1)~The programmer writes a method \code{constructFrom}
    that initializes \this from a parameter.
(This is similar to a copy-constructor in \CC,
    and indeed this method should be given all the privileges of a
    constructor, such as assignment to \code{final} fields.)
(2)~The compiler automatically generates a \code{clone} method
    that first nullifies all the reference fields
    and then calls the user generated \code{constructFrom} method.
This approach enforces the ownership and immutability guarantees.


% LocalWords:  CaseStudy util cJ's wildcards OIGJ's ThisI NodeO NodeI Immut IGJ
% LocalWords:  OImmut OReadOnly prev keySet LinkedHashMap accessOrder readonly
% LocalWords:  constructFrom ItrI CollectionI ReadOnly OGJ
